rev(${\it as}$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$rec{-}case(${\it as}$) of [] =$>$ [] $\mid$ $a$::${\it as'}$ =$>$ .rev(${\it as'}$) @ [$a$]
\\[0ex]
\\[0ex]{\em clarification:}
\\[0ex]
\\[0ex]rev(${\it as}$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$rec{-}case(${\it as}$) of [] =$>$ [] $\mid$ $a$::${\it as'}$ =$>$ .rev(${\it as'}$) @ [$a$ / []]
\\[0ex]\emph{(recursive)}